Left Termination proof of /tmp/tmplGW8wL/at.pl

Left Termination of the query pattern at_in_2(a, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

at(X, fido) :- ','(at(X, mary), near(X)).
at(ta, mary).
at(jm, mary).
near(jm).

Queries:

at(a,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
at_in: (f,f) (f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)
AT_IN_AG(x1, x2) = AT_IN_AG(x2)
U2_AG(x1, x2) = U2_AG(x1, x2)
U1_AA(x1, x2) = U1_AA(x2)
U2_AA(x1, x2) = U2_AA(x1, x2)
NEAR_IN_G(x1) = NEAR_IN_G(x1)
AT_IN_AA(x1, x2) = AT_IN_AA
U1_AG(x1, x2) = U1_AG(x2)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2) = at_in_aa
U1_aa(x1, x2) = U1_aa(x2)
at_in_ag(x1, x2) = at_in_ag(x2)
fido = fido
U1_ag(x1, x2) = U1_ag(x2)
mary = mary
at_out_ag(x1, x2) = at_out_ag(x1)
U2_ag(x1, x2) = U2_ag(x1, x2)
near_in_g(x1) = near_in_g(x1)
jm = jm
near_out_g(x1) = near_out_g
U2_aa(x1, x2) = U2_aa(x1, x2)
at_out_aa(x1, x2) = at_out_aa(x1, x2)
AT_IN_AG(x1, x2) = AT_IN_AG(x2)
U2_AG(x1, x2) = U2_AG(x1, x2)
U1_AA(x1, x2) = U1_AA(x2)
U2_AA(x1, x2) = U2_AA(x1, x2)
NEAR_IN_G(x1) = NEAR_IN_G(x1)
AT_IN_AA(x1, x2) = AT_IN_AA
U1_AG(x1, x2) = U1_AG(x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 0 SCCs with 8 less nodes.